#!/usr/bin/python

# x + 5
expressions = [
(2, "(max(((17 - (v0 % 4))/4), ((max(((min((v1*2), ((v0 % 2) + 5)) + (v0/2))/2), ((v0/4) + v1)) - (((v0 + -6)/4) + v1)) + 2)) <= 1024)"),
(2, "(max(((17 - (v0 % 4))/4), ((((min((v1*2), ((v0 % 2) + 20)) + (v0/2))/2) - (((v0 + -6)/4) + v1)) + 2)) <= 1024)"),
(3, "((max(((8 - (((v0*161) + v1) % 2))/2), ((((min((v2*2), 159) + ((v0*161) + v1))/2) - (((((v0*161) + v1) + -3)/2) + v2)) + 2)) <= 1024))"),
(2, "((((v0 + v1)/2) <= (min((((v0 + v1) % 2)*2), 1) + ((v0 + v1)/2))) && (((max((((v0 + v1) % 2)*2), 1) + ((v0 + v1)/2)) + -2) <= ((v0 + v1)/2)))"),
(2, "((((v0 - v1)/4) + 1) <= max((((v0 - v1) + 5)/4), 0))"),
(2, "((((v0 - v1)/8) + 1) <= max((((v0 - v1) + 9)/8), 0))"),
(2, "((((v0 - v1)/8) + 32) <= max((((v0 - v1) + 257)/8), 0))"),
(2, "((((v0 - v1)/8) + 96) <= max((((v0 - v1) + 769)/8), 0))"),
(2, "(((((v0 - v1) + 98)/97)*97) <= (min(((((v0 - v1) + 98)/97)*97), 8) + (((max(((((v0 - v1) + 98)/97)*97), 8) + -1)/8)*8)))"),
(2, "((v0 + -11) <= ((((v0 - v1)/12)*12) + v1))"),
(2, "((((((v0 + 129)/2) - v1)/4) + -1) <= max(((((v0 + 123)/2) - v1)/4), -1))"),
(2, "(((v0 + -1)/2) <= ((((((v0 + 1)/2) - v1)/2)*2) + v1))"),
(1, "(((v0 + 1)/2) <= ((v0/2) + ((((v0 % 2) + 3)/4)*4)))"),
(2, "((((((v0 + 1)/2) - v1)/2) + -1) <= max(((((v0 + -1)/2) - v1)/2), -1))"),
(2, "((((((v0 + 1)/2) - v1)/5) + -1) <= max(((((v0 + -7)/2) - v1)/5), -1))"),
(6, "(((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min(((v3 - v4)/104), v5)*104) + v4) <= (max(((v5*104) + (v4 - v3)), -103) + min((((v5*104) + v4) + 103), v3))))"),
(6, "(((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min((v3 - ((v4*16) + v5)), 15) + (v4*16)) + v5) <= min((((v4*16) + v5) + 15), v3)))"),
(6, "(((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min(((v3 - v4)/16), v5)*16) + v4) <= (max(((v5*16) + (v4 - v3)), -15) + min((((v5*16) + v4) + 15), v3))))"),
(6, "(((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min((v3 - ((v4*32) + v5)), 16) + (v4*32)) + v5) <= min((((v4*32) + v5) + 16), v3)))"),
(6, "(((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min((v3 - ((v4*52) + v5)), 51) + (v4*52)) + v5) <= min((((v4*52) + v5) + 51), v3)))"),
(6, "(((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min(((v3 - v4)/52), v5)*52) + v4) <= (max(((v5*52) + (v4 - v3)), -51) + min((((v5*52) + v4) + 51), v3))))"),
(7, "(((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min((v3 - (((v4 + v5)*16) + v6)), 15) + ((v4 + v5)*16)) + v6) <= min(((((v4 + v5)*16) + v6) + 15), v3)))"),
(2, "((((((v0 + 161)/2) - v1)/4) + -1) <= max(((((v0 + 155)/2) - v1)/4), -1))"),
(3, "((((((((v0*161) + v1) + 161)/2) - v2)/4) + -1) <= max(((((((v0*161) + v1) + 155)/2) - v2)/4), -1))"),
(3, "((((((((v0*161) + v1) + 161)/2) - v2)/42) + -1) <= max(((((((v0*161) + v1) + 79)/2) - v2)/42), -1))"),
(2, "((((((v0 + 163)/2) - v1)/4) + -1) <= max(((((v0 + 157)/2) - v1)/4), -1))"),
(2, "((v0 + -17) <= ((((v0 - v1)/18)*18) + v1))"),
(2, "((((((v0 + 193)/2) - v1)/8) + -1) <= max(((((v0 + 179)/2) - v1)/8), -1))"),
(2, "((v0 + -1) <= (max(v1, 0) + (((v0 - max(v1, 0))/2)*2)))"),
(2, "((v0 + -1) <= ((((v0 - v1)/2)*2) + v1))"),
(2, "(((v0/2) + -14) <= (((v1 + -126)/64) + (((((v0/2) - ((v1 + -126)/64)) + 1)/16)*16)))"),
(1, "(((v0/2) + 1) <= max(((v0 + 3)/2), 0))"),
(1, "(((v0/2) <= (min(((v0 % 2)*2), 1) + (v0/2))) and (((max(((v0 % 2)*2), 1) + (v0/2)) + -2) <= (v0/2)))"),
(3, "(((((v0/2) + (min((v1 - (v2*161)), 160) + (min((v1/161), v2)*161))) + 1)/2) <= (((min(((v2*161) + 160), v1) + (v0/2)) + 1)/2))"),
(3, "(((((v0/2) + (min((v1 - (v2*81)), 80) + (min((v1/81), v2)*81))) + 1)/2) <= (((min(((v2*81) + 80), v1) + (v0/2)) + 1)/2))"),
(2, "((v0 + -2) <= ((((v0 - v1)/3)*3) + v1))"),
(2, "((((((v0 + 321)/2) - v1)/41) + -1) <= max(((((v0 + 241)/2) - v1)/41), -1))"),
(2, "((((((v0 + 321)/2) - v1)/4) + -1) <= max(((((v0 + 315)/2) - v1)/4), -1))"),
(2, "((((((v0 + 321)/2) - v1)/8) + -1) <= max(((((v0 + 307)/2) - v1)/8), -1))"),
(3, "((((((((v0*321) + v1) + 321)/2) - v2)/82) + -1) <= max(((((((v0*321) + v1) + 159)/2) - v2)/82), -1))"),
(3, "((((((v0*321) + v1) - v2)/2) + 160) <= max((((((v0*321) + v1) - v2) + 321)/2), 0))"),
(2, "((((((v0 + 3)/2) - v1)/2) + -1) <= max(((((v0 + 1)/2) - v1)/2), -1))"),
(2, "((v0 + -3) <= (max(v1, 0) + (((v0 - max(v1, 0))/4)*4)))"),
(2, "((v0 + -40) <= ((((v0 - v1)/41)*41) + v1))"),
(4, "((((v0*40) + (((v1 + 165)/4) + (v2*160))) + -3) <= ((((v0*10) + (((((v1 + 165)/4) - v3)/4) + (v2*40)))*4) + v3))"),
(5, "((((((v0*4) + ((((min(v1, 53) + v2) + -115)/64) + (v3*2))) + -1) <= ((((min(v1, 53) + v2) + -179)/64) + (((v0*2) + v3)*2))) and ((v4/2) <= (min(((v4 % 2)*2), 1) + (v4/2)))) and (((max(((v4 % 2)*2), 1) + (v4/2)) + -2) <= (v4/2)))"),
(2, "((v0 + -4) <= ((((v0 - v1)/5)*5) + v1))"),
(4, "((((v0*4) + (((v1 + 9)/2) + (v2*640))) + -1) <= ((((v0*2) + (((((v1 + 9)/2) - v3)/2) + (v2*320)))*2) + v3))"),
(2, "((((((v0 + 51)/2) - v1)/16) + -1) <= max(((((v0 + 21)/2) - v1)/16), -1))"),
(2, "((v0 + -5) <= ((((v0 - v1)/6)*6) + v1))"),
(2, "((((((v0 + 641)/2) - v1)/4) + -1) <= max(((((v0 + 635)/2) - v1)/4), -1))"),
(2, "((v0 + -70) <= ((((v0 - v1)/71)*71) + v1))"),
(2, "((((v0 + 738)/32) + ((v1/26)*26)) <= (((v0 + 34)/32) + ((((((v0 + 738)/32) + ((v1/26)*26)) - ((v0 + -62)/32))/4)*4)))"),
(2, "((((((v0 + 81)/2) - v1)/11) + -1) <= max(((((v0 + 61)/2) - v1)/11), -1))"),
(3, "((((((((v0*81) + v1) + 81)/2) - v2)/11) + -1) <= max(((((((v0*81) + v1) + 61)/2) - v2)/11), -1))"),
(2, "((v0 + -8) <= ((((v0 - v1)/9)*9) + v1))"),
(4, "((((v0*8) + (((v1 + 17)/2) + (v2*640))) + -1) <= ((((v0*4) + (((((v1 + 17)/2) - v3)/2) + (v2*320)))*2) + v3))"),
(2, "(v0 <= max(max(v0, v1), (max(v1, 0) + 1)))"),
(2, "((max(min((v0 + -2), (min(((v0 + -1)), 0))), 0) + -1) <= max((max(v1, 0) + 1), v1))"),
(3, "(max(min(((v0 + v1) + -1), v2), v1) <= max(min((v0 + v1), v2), (v1 + 1)))"),
(1, "(max(((v0 + -1)/2), (((v0 + -3)/2) + (((v0 + 1) % 2)*2))) <= ((v0 + 1)/2))"),
(3, "(max((((((v0*161) + v1) + v2) + -1)/2), ((((((v0*161) + v1) + v2) + -3)/2) + ((((((v0*161) + v1) + v2) + 1) % 2)*2))) <= (((((v0*161) + v1) + v2) + 1)/2))"),
(1, "((max((v0/2), -2) + 1) <= max(((v0 + 3)/2), 0))"),
(3, "(max((((((v0*41) + v1) + v2) + -1)/2), ((((((v0*41) + v1) + v2) + -3)/2) + ((((((v0*41) + v1) + v2) + 1) % 2)*2))) <= (((((v0*41) + v1) + v2) + 1)/2))"),
(3, "(max((((((v0*81) + v1) + v2) + -1)/2), ((((((v0*81) + v1) + v2) + -3)/2) + ((((((v0*81) + v1) + v2) + 1) % 2)*2))) <= (((((v0*81) + v1) + v2) + 1)/2))"),
(2, "(max(((v0 - v1)/2), -1) <= max((((v0 - v1) + 1)/2), 0))"),
(9, "(min(min(min((min((v0 - ((v1*144) + v2)), v3) + 1), v3), (v3 + 2)), (min(min(min(v4, v5), ((((v6 + v7) + -29)/2) - ((v1*144) + v2))), v8) + 16)) <= 14)"),
(5, "((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + -1)/8)*8)), (v3 + -8)) + -18) <= (((((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + 7)/8)*8)), v3) - v4) + -1)/26)*26) + v4))"),
(5, "(((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + -1)/8)*8)), (v3 + -8)) + 5)/2) <= ((v4/2) + ((((((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + 7)/8)*8)), v3) + 1)/2) - (v4/2)) + 1)/4)*4)))"),
(3, "(((min((((min(v0, 101) + v1) + -227)/64), ((v2 + -29)/2)) + 1) <= (min((((min(v0, 101) + v1) + -163)/32), (v2 + -8))/2)))"),
(3, "(((min(((((min(v0, 101) + v1) + -163)/32) + ((((v2 - (((min(v0, 101) + v1) + -163)/32)) + -1)/8)*8)), (v2 + -8)) + -21)/2) <= min(((v2 + -29)/2), ((((min(v0, 101) + v1) + -227)/64) + (((((v2 + 1)/2) - (((min(v0, 101) + v1) + -227)/64))/16)*16))))"),
(4, "(((min((((min(v0, 11) + v1) + -25)/8), ((v2 + -23)/4)) + 1) <= (min((((min(v0, 11) + v1) + -17)/4), ((v2 + -13)/2))/2)) and (((min(((v2 + -13)/2), ((((min(v0, 11) + v1) + -17)/4) + ((((min((((v0 + v1) + 5)/2), v3)/2) - (((min(v0, 11) + v1) + -17)/4))/8)*8))) + -5)/2) <= min(((v2 + -23)/4), ((((min(v0, 11) + v1) + -25)/8) + (((((v2 + 5)/4) - (((min(v0, 11) + v1) + -25)/8))/8)*8)))))"),
(6, "((((min((((min(v0, 11) + v1) + -25)/8), ((v2 + -23)/4)) + 1) <= (min((((min(v0, 11) + v1) + -17)/4), ((v2 + -13)/2))/2)) and (((min(((v2 + -13)/2), ((((min(v0, 11) + v1) + -17)/4) + ((((min((((v0 + v1) + 5)/2), v3)/2) - (((min(v0, 11) + v1) + -17)/4))/8)*8))) + -5)/2) <= min(((v2 + -23)/4), ((((min(v0, 11) + v1) + -25)/8) + (((((v2 + 5)/4) - (((min(v0, 11) + v1) + -25)/8))/8)*8))))) and (((v4 + 1)/4) <= ((((((v4 + 5)/4) - v5)/2)*2) + v5)))"),
(3, "(((min((((min(v0, 11) + v1) + -41)/16), ((v2 + -43)/8)) + 1) <= (min((((min(v0, 11) + v1) + -25)/8), ((v2 + -23)/4))/2)) and (((min(((v2 + -23)/4), ((((min(v0, 11) + v1) + -25)/8) + (((((v2 + 5)/4) - (((min(v0, 11) + v1) + -25)/8))/8)*8))) + -5)/2) <= min(((v2 + -43)/8), ((((min(v0, 11) + v1) + -41)/16) + (((((v2 + 13)/8) - (((min(v0, 11) + v1) + -41)/16))/8)*8)))))"),
(5, "(((min(((((min(v0, 17) + v1) + -23)/4) + (((v2 + -1)/8)*8)), (v3 + -8)) + -183)/2) <= ((v4/2) + ((((((min(((((min(v0, 17) + v1) + -23)/4) + (((v2 + 7)/8)*8)), v3) + 1)/2) - (v4/2)) + 1)/98)*98)))"),
(3, "(((min((((min(v0, 17) + v1) + -31)/8), ((v2 + -13)/2)) + 1) <= (min((((min(v0, 17) + v1) + -23)/4), (v2 + -8))/2)) and (((min(((((min(v0, 17) + v1) + -23)/4) + ((((v2 - (((min(v0, 17) + v1) + -23)/4)) + -1)/8)*8)), (v2 + -8)) + -5)/2) <= min(((v2 + -13)/2), ((((min(v0, 17) + v1) + -31)/8) + (((((v2 + 1)/2) - (((min(v0, 17) + v1) + -31)/8))/8)*8)))))"),
(3, "(((min((((min(v0, 17) + v1) + -47)/16), ((v2 + -23)/4)) + 1) <= (min((((min(v0, 17) + v1) + -31)/8), ((v2 + -13)/2))/2)) and (((min(((v2 + -13)/2), ((((min(v0, 17) + v1) + -31)/8) + (((((v2 + 1)/2) - (((min(v0, 17) + v1) + -31)/8))/8)*8))) + -5)/2) <= min(((v2 + -23)/4), ((((min(v0, 17) + v1) + -47)/16) + (((((v2 + 5)/4) - (((min(v0, 17) + v1) + -47)/16))/8)*8)))))"),
(5, "(((min(((((min(v0, 29) + v1) + -43)/8) + (((v2 + -1)/8)*8)), (v3 + -8)) + -87)/2) <= ((v4/2) + ((((((min(((((min(v0, 29) + v1) + -43)/8) + (((v2 + 7)/8)*8)), v3) + 1)/2) - (v4/2)) + 1)/50)*50)))"),
(3, "(((min((((min(v0, 29) + v1) + -59)/16), ((v2 + -13)/2)) + 1) <= (min((((min(v0, 29) + v1) + -43)/8), (v2 + -8))/2)) and (((min(((((min(v0, 29) + v1) + -43)/8) + ((((v2 - (((min(v0, 29) + v1) + -43)/8)) + -1)/8)*8)), (v2 + -8)) + -5)/2) <= min(((v2 + -13)/2), ((((min(v0, 29) + v1) + -59)/16) + (((((v2 + 1)/2) - (((min(v0, 29) + v1) + -59)/16))/8)*8)))))"),
(3, "(((min((((min(v0, 29) + v1) + -91)/32), ((v2 + -23)/4)) + 1) <= (min((((min(v0, 29) + v1) + -59)/16), ((v2 + -13)/2))/2)) and (((min(((v2 + -13)/2), ((((min(v0, 29) + v1) + -59)/16) + (((((v2 + 1)/2) - (((min(v0, 29) + v1) + -59)/16))/8)*8))) + -5)/2) <= min(((v2 + -23)/4), ((((min(v0, 29) + v1) + -91)/32) + (((((v2 + 5)/4) - (((min(v0, 29) + v1) + -91)/32))/8)*8)))))"),
(3, "((min((min((v0*4), 3) + v1), v2) <= ((v0*4) + v1)) and ((min((v0*4), 3) + v1) <= ((((((min((v0*4), 3) + v1) - v2) + 3)/4)*4) + v2)))"),
(3, "(((min((((min(v0, 53) + v1) + -115)/32), ((v2 + -13)/2)) + 1) <= (min((((min(v0, 53) + v1) + -83)/16), (v2 + -8))/2)) and (((min(((((min(v0, 53) + v1) + -83)/16) + ((((v2 - (((min(v0, 53) + v1) + -83)/16)) + -1)/8)*8)), (v2 + -8)) + -5)/2) <= min(((v2 + -13)/2), ((((min(v0, 53) + v1) + -115)/32) + (((((v2 + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/8)*8)))))"),
(3, "(((min((((min(v0, 53) + v1) + -179)/64), ((v2 + -55)/4)) + 1) <= (min((((min(v0, 53) + v1) + -115)/32), ((v2 + -13)/2))/2)) and (((min(((v2 + -13)/2), ((((min(v0, 53) + v1) + -115)/32) + (((((v2 + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/8)*8))) + -21)/2) <= min(((v2 + -55)/4), ((((min(v0, 53) + v1) + -179)/64) + (((((v2 + 5)/4) - (((min(v0, 53) + v1) + -179)/64))/16)*16)))))"),
(5, "((min(((((min(v0, 53) + v1) + -83)/16) + (((v2 + -1)/8)*8)), (v3 + -8)) + -42) <= (((((min(((((min(v0, 53) + v1) + -83)/16) + (((v2 + 7)/8)*8)), v3) - v4) + -1)/50)*50) + v4))"),
(4, "((min(min((v0 - (v1*117)), v2), 116) + (min(((v0 - v2)/117), v1)*117)) <= v3)"),
(4, "((min(min((v0 - (v1*161)), v2), 160) + (min(((v0 - v2)/161), v1)*161)) <= v3)"),
(2, "((((min((v0 + 10), v1)/2) + -5) <= (v0/2)) and (((v1/2) + -5) <= ((v0/2) + (((((v1/2) - (v0/2)) + 2)/8)*8))))"),
(2, "(((min((v0 + 11), v1) + -13)/2) <= ((v1 + -13)/2))"),
(2, "(((min((v0 + -11), v1)/2) <= (min((v0 + -8), v1)/2)) and (((min((((((v0 - v1) + -1)/8)*8) + v1), (v0 + -8)) + -5)/2) <= min(((v0 + -13)/2), (((v1/2) + ((((((v0 + 1)/2) - (v1/2)) + 1)/8)*8)) + -1))))"),
(3, "(((((min(v0, 11) + v1) + 367)/4) + ((v2/97)*97)) <= ((((min(v0, 11) + v1) + 755)/4) + (((((((min(v0, 11) + v1) + 367)/4) + ((v2/97)*97)) - (((min(v0, 11) + v1) + -17)/4))/194)*194)))"),
(5, "((min(((v0 + -13)/2), ((((min(v1, 11) + v2) + -17)/4) + ((v3/8)*8))) + -186) <= (((((min(((v0 + 3)/2), ((((min(v1, 11) + v2) + 15)/4) + ((v3/8)*8))) - v4) + -1)/194)*194) + v4))"),
(5, "(((min(((v0 + -13)/2), ((((min(v1, 17) + v2) + -31)/8) + ((v3/8)*8))) + -87)/2) <= ((v4/2) + ((((((min(((v0 + 3)/2), ((((min(v1, 17) + v2) + 33)/8) + ((v3/8)*8))) + 1)/2) - (v4/2)) + 1)/50)*50)))"),
(5, "((min(((v0 + -13)/2), ((((min(v1, 17) + v2) + -31)/8) + ((v3/8)*8))) + -90) <= (((((min(((v0 + 3)/2), ((((min(v1, 17) + v2) + 33)/8) + ((v3/8)*8))) - v4) + -1)/98)*98) + v4))"),
(5, "(((min(((v0 + -13)/2), ((((min(v1, 29) + v2) + -59)/16) + ((v3/8)*8))) + -39)/2) <= ((v4/2) + ((((((min(((v0 + 3)/2), ((((min(v1, 29) + v2) + 69)/16) + ((v3/8)*8))) + 1)/2) - (v4/2)) + 1)/26)*26)))"),
(5, "(((min(((v0 + -13)/2), ((((min(v1, 53) + v2) + -115)/32) + ((v3/8)*8))) + -15)/2) <= ((v4/2) + ((((((min(((v0 + 3)/2), ((((min(v1, 53) + v2) + 141)/32) + ((v3/8)*8))) + 1)/2) - (v4/2)) + 1)/14)*14)))"),
(5, "((min(((v0 + -13)/2), ((((min(v1, 53) + v2) + -115)/32) + ((v3/8)*8))) + -18) <= (((((min(((v0 + 3)/2), ((((min(v1, 53) + v2) + 141)/32) + ((v3/8)*8))) - v4) + -1)/26)*26) + v4))"),
(3, "(min((((v0*144) + v1) + 128), v2) <= min(((min(((min((v2 - ((v0*144) + v1)), 128) + 15)/16), 8)*16) + ((v0*144) + v1)), v2))"),
(3, "((min((((v0*144) + v1) + 136), v2) + -8) <= ((((min((v2 - ((v0*144) + v1)), 136) + 7)/16)*16) + ((v0*144) + v1)))"),
(3, "((min((((v0*144) + v1) + 139), v2) + -11) <= ((((min((v2 - ((v0*144) + v1)), 139) + 4)/16)*16) + ((v0*144) + v1)))"),
(3, "((min((((v0*144) + v1) + 140), v2) + -12) <= ((((min((v2 - ((v0*144) + v1)), 140) + 3)/16)*16) + ((v0*144) + v1)))"),
(3, "((min((((v0*144) + v1) + 142), v2) + -14) <= ((((min((v2 - ((v0*144) + v1)), 142) + 1)/16)*16) + ((v0*144) + v1)))"),
(3, "((min((((v0*144) + v1) + 142), v2) + -70) <= ((((min((v2 - ((v0*144) + v1)), 142) + 1)/72)*72) + ((v0*144) + v1)))"),
(2, "(((min(((v0 + -14)/8), (((((v0 + -10)/4) + v1)/2) + -6)) + 1) <= (min(((v0 + -6)/4), (((v0 + -38)/4) + v1))/2)) and (((min((((v0 + -6)/4) + ((((((v0 + -10)/4) + v1) - ((v0 + -6)/4))/8)*8)), (((v0 + -38)/4) + v1)) + -5)/2) <= min((((v0 + -14)/8) + ((((((((v0 + -10)/4) + v1)/2) - ((v0 + -14)/8)) + 1)/8)*8)), (((((v0 + -10)/4) + v1)/2) + -6))))"),
(2, "((((min((v0 + 17), v1) + -23)/4) <= ((min((v0 + 11), v1) + -17)/4)) and (((min(((v1 + -13)/2), (((v0/2) + ((((((v1 + 1)/2) - (v0/2)) + 1)/8)*8)) + -1)) + -5)/2) <= min(((v1 + -23)/4), (((v0 + -6)/4) + (((((v1 + 5)/4) - ((v0 + -6)/4))/8)*8)))))"),
(5, "(((((min(((v0*193) + 10), v1) + (v2/2)) + -3)/2) <= ((min(((v0*193) + 7), v1) + (v2/2))/2)) and (((min(((((min((v1 - (v0*193)), 192)/8)*8) + v3) + 7), v4) + -13)/2) <= min(((v4 + -13)/2), (((v3 + -3)/2) + (((((v4 + 1)/2) - ((v3 + -3)/2))/8)*8)))))"),
(2, "(((min((((v0/2) % 2)*2), 1) + ((v0/4) + v1)) + -1) <= (((v0 + 6)/4) + v1))"),
(4, "((min((((v0 + 22)/4) + ((v1/8)*8)), v2) + -193) <= ((((min((((v0 + 22)/4) + ((v1/8)*8)), v2) - v3)/194)*194) + v3))"),
(5, "(((min(((v0 + -23)/4), ((((min(v1, 17) + v2) + -47)/16) + ((v3/8)*8))) + -39)/2) <= ((v4/2) + ((((((min(((v0 + 9)/4), ((((min(v1, 17) + v2) + 81)/16) + ((v3/8)*8))) + 1)/2) - (v4/2)) + 1)/26)*26)))"),
(5, "((min(((v0 + -23)/4), ((((min(v1, 29) + v2) + -91)/32) + ((v3/8)*8))) + -18) <= (((((min(((v0 + 9)/4), ((((min(v1, 29) + v2) + 165)/32) + ((v3/8)*8))) - v4) + -1)/26)*26) + v4))"),
(2, "(((min(((v0 + -23)/4), ((v1/8) + -3)) + 1) <= (min(((v0 + -13)/2), ((v1/4) + -4))/2)) and (((min(((v0 + -13)/2), (((v1/4) + ((((((v0 + 1)/2) - (v1/4)) + 4)/8)*8)) + -4)) + -5)/2) <= min(((v0 + -23)/4), (((v1/8) + ((((((v0 + 5)/4) - (v1/8)) + 3)/8)*8)) + -3))))"),
(2, "(((min(((v0 + -25)/8), ((v1 + -55)/4)) + 1) <= (min(((v0 + -17)/4), ((v1 + -13)/2))/2)) and (((min(((v1 + -13)/2), (((v0 + -17)/4) + (((((v1 + 1)/2) - ((v0 + -17)/4))/8)*8))) + -21)/2) <= min(((v1 + -55)/4), (((v0 + -25)/8) + (((((v1 + 5)/4) - ((v0 + -25)/8))/16)*16)))))"),
(2, "(((min((v0 + 27), v1) + -29)/2) <= ((v1 + -29)/2))"),
(2, "(((min((v0 + -27), v1)/2) <= (min((v0 + -16), v1)/2)) and (((min((((((v0 - v1) + -1)/16)*16) + v1), (v0 + -16)) + -13)/2) <= min(((v0 + -29)/2), (((v1/2) + ((((((v0 + 1)/2) - (v1/2)) + 1)/16)*16)) + -1))))"),
(2, "(((min((v0 + -27), v1)/2) <= (min((v0 + -8), v1)/2)) and (((min((((((v0 - v1) + -1)/8)*8) + v1), (v0 + -8)) + -21)/2) <= min(((v0 + -29)/2), (((v1/2) + ((((((v0 + 1)/2) - (v1/2)) + 1)/16)*16)) + -1))))"),
(5, "((min(((v0 + -29)/2), ((((min(v1, 101) + v2) + -227)/64) + ((v3/16)*16))) + 2) <= (((((min(((v0 + 3)/2), ((((min(v1, 101) + v2) + 797)/64) + ((v3/16)*16))) - v4) + -1)/14)*14) + v4))"),
(5, "(((min(((v0 + -29)/2), ((((min(v1, 101) + v2) + -227)/64) + ((v3/16)*16))) + 5)/2) <= ((v4/2) + ((((((min(((v0 + 3)/2), ((((min(v1, 101) + v2) + 797)/64) + ((v3/16)*16))) + 1)/2) - (v4/2)) + 1)/8)*8)))"),
(1, "(min((v0 + -2), (min(((v0 + -1)), 0))) <= 0)"),
(4, "((min((((((v0*2) + v1)*144) + v2) + 140), v3) + -12) <= ((((min((v3 - ((((v0*2) + v1)*144) + v2)), 140) + 3)/16)*16) + ((((v0*2) + v1)*144) + v2)))"),
(4, "((min((((((v0*2) + v1)*144) + v2) + 142), v3) + -14) <= ((((min((v3 - ((((v0*2) + v1)*144) + v2)), 142) + 1)/16)*16) + ((((v0*2) + v1)*144) + v2)))"),
(3, "(((min(((v0/2) + (v1*161)), v2) + -3)/2) <= ((v2 + -3)/2))"),
(4, "(((min((((v0/2) + (((v1 + 1)/8)*8)) + 6), v2)/2) + 1) <= (((v3 + 377)/2) + (((((min((((v0/2) + (((v1 + 9)/8)*8)) + -2), v2)/2) - ((v3 + -9)/2)) + 1)/194)*194)))"),
(2, "((((min((v0 + 2), v1)/2) + -1) <= (v0/2)) and (((v1/2) + -1) <= ((v0/2) + (((((v1/2) - (v0/2)) + 2)/4)*4))))"),
(3, "(((min(((v0/2) + (v1*321)), v2) + -3)/2) <= ((v2 + -3)/2))"),
(3, "(((min(((v0/2) + (v1*41)), v2) + -3)/2) <= ((v2 + -3)/2))"),
(3, "(((min(((v0/2) + (v1*81)), v2) + -3)/2) <= ((v2 + -3)/2))"),
(5, "((min(((v0*31) + ((v1*4) + v2)), (v3 + -1)) + ((v4 + -6)/4)) < (((v4 + -2)/4) + ((v0*31) + ((v1*4) + v2))))"),
(4, "((min((((v0 + -3)/2) + (((v1 + 1)/8)*8)), ((v2/2) + -6)) + -36) <= ((v3/2) + ((((min((((v0 + -3)/2) + (((v1 + 9)/8)*8)), ((v2/2) + 2)) - (v3/2)) + 5)/50)*50)))"),
(2, "((min((v0 + 3), v1)/2) <= (v1/2))"),
(2, "((((min((v0 + 41), v1) + -38)/4) <= (min((v0 + 3), v1)/4)) and (((min((((v0 + -9)/2) + (((((v1/2) - ((v0 + -9)/2)) + 1)/8)*8)), ((v1/2) + -6)) + -21)/2) <= min(((v1 + -54)/4), (((v0 + -13)/4) + (((((v1 + 6)/4) - ((v0 + -13)/4))/16)*16)))))"),
(2, "((((min((v0 + 49), v1) + -55)/4) <= ((min((v0 + 11), v1) + -17)/4)) and (((min(((v1 + -13)/2), (((v0/2) + ((((((v1 + 1)/2) - (v0/2)) + 1)/8)*8)) + -1)) + -21)/2) <= min(((v1 + -55)/4), (((v0 + -6)/4) + (((((v1 + 5)/4) - ((v0 + -6)/4))/16)*16)))))"),
(3, "((min((((v0 + 5)/2) + v1), ((((((((v0 + 3)/2) + v1) - v2)/2)*2) + v2) + 2)) + -1) <= (((v0 + 3)/2) + v1))"),
(2, "(min(((v0 + -6)/4), (min(v1, 49) + ((v0 + -38)/4))) <= min(((v0 + -6)/4), (((v0 + -38)/4) + v1)))"),
(2, "(min(((v0 + -6)/4), (((v0 + -38)/4) + v1)) <= min(((v0 + -6)/4), (min(v1, 49) + ((v0 + -38)/4))))"),
(4, "(((min((((v0 + -6)/4) + (((v1 + 1)/8)*8)), ((v2/2) + -6)) + -85)/2) <= ((v3/2) + ((((((min((((v0 + -6)/4) + (((v1 + 9)/8)*8)), ((v2/2) + 2)) + 1)/2) - (v3/2)) + 1)/49)*49)))"),
(4, "(min((((v0 + -6)/4) + ((v1/8)*8)), (((v0 + -38)/4) + v2)) <= min((((v1/8)*8) + (((v0 + -6)/4) + (max((v3/49), 0)*49))), (((v0 + -38)/4) + v2)))"),
(3, "(((min((((v0 + -6)/4) + v1), (v2 + 6))/2) + -3) <= (v2/2))"),
(3, "(((min((v0 + 6), ((v1/2) + v2)) + -3)/2) <= ((v0 + 3)/2))"),
(5, "((min(((v0*81) + ((v1*41) + v2)), (v3 + -1)) + ((v4 + -6)/4)) < (((v4 + -2)/4) + ((v0*81) + ((v1*41) + v2))))"),
(5, "((min(((v0*81) + ((v1*8) + v2)), (v3 + -1)) + ((v4 + -6)/4)) < (((v4 + -2)/4) + ((v0*81) + ((v1*8) + v2))))"),
(2, "((((min((v0 + 9), v1) + -6)/4) <= (min((v0 + 3), v1)/4)) and (((min((((v0 + -9)/2) + (((((v1/2) - ((v0 + -9)/2)) + 1)/8)*8)), ((v1/2) + -6)) + -5)/2) <= min(((v1 + -22)/4), (((v0 + -13)/4) + (((((v1 + 6)/4) - ((v0 + -13)/4))/8)*8)))))"),
(9, "(min((((v0 + v1)*117) + (min(((v2*59) + (((v3*4) + v4) + v5)), v6) + v7)), v8) <= (((v0 + v1)*117) + (((v2*59) + (((v3*4) + v4) + v5)) + v7)))"),
(3, "(((min((((v0 + v1) + -13)/2), (((v1/2) + (((v2 + 1)/8)*8)) + -1)) + 9)/2) <= ((((min(v0, 11) + v1) + 367)/4) + ((((min((((v0 + v1) + 5)/2), ((v1/2) + (((v2 + 9)/8)*8)))/2) - (((min(v0, 11) + v1) + -17)/4))/97)*97)))"),
(3, "(((min((((v0 + v1) + -13)/2), (((v1/2) + (((v2 + 1)/8)*8)) + -1)) + 9)/2) <= ((((min(v0, 11) + v1) + 755)/4) + ((((min((((v0 + v1) + 5)/2), ((v1/2) + (((v2 + 9)/8)*8)))/2) - (((min(v0, 11) + v1) + -17)/4))/194)*194)))"),
(3, "((min((((((v0 - v1)/16)*16) + v1) + 15), v0) + -142) <= ((((min((((((v0 - v1)/16)*16) + v1) + 15), v0) - v2)/143)*143) + v2))"),
(3, "((min((((((v0 - v1)/16)*16) + v1) + 15), v0) + -70) <= ((((min((((((v0 - v1)/16)*16) + v1) + 15), v0) - v2)/71)*71) + v2))"),
(9, "(min((((v0 + v1)*161) + (min(((v2*81) + (((v3*2) + v4) + v5)), v6) + v7)), v8) <= (((v0 + v1)*161) + (((v2*81) + (((v3*2) + v4) + v5)) + v7)))"),
(9, "(min((((v0 + v1)*161) + (min(((v2*81) + (((v3*4) + v4) + v5)), v6) + v7)), v8) <= (((v0 + v1)*161) + (((v2*81) + (((v3*4) + v4) + v5)) + v7)))"),
(6, "(min((((v0 + v1)*161) + (min(v2, v3) + v4)), v5) <= (((v0 + v1)*161) + (v2 + v4)))"),
(3, "((min((((v0 + v1) + -163)/32), (((v1 + -62)/32) + ((v2/8)*8))) + 7) <= ((((min(v0, 101) + v1) + 221)/32) + ((((min((((v0 + v1) + 93)/32), (((v1 + 194)/32) + ((v2/8)*8))) - (((min(v0, 101) + v1) + -163)/32)) + -1)/13)*13)))"),
(3, "((min((((v0 + v1) + -163)/32), (((v1 + -62)/32) + ((v2/8)*8))) + 7) <= ((((min(v0, 101) + v1) + 637)/32) + ((((min((((v0 + v1) + 93)/32), (((v1 + 194)/32) + ((v2/8)*8))) - (((min(v0, 101) + v1) + -163)/32)) + -1)/26)*26)))"),
(3, "(((min((((v0 + v1) + -163)/32), (((v1 + -62)/32) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 101) + v1) + -35)/64) + (((((min((((v0 + v1) + 93)/32), (((v1 + 194)/32) + ((v2/8)*8))) + 1)/2) - (((min(v0, 101) + v1) + -227)/64))/4)*4)))"),
(3, "(((min((((v0 + v1) + -163)/32), (((v1 + -62)/32) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 101) + v1) + 605)/64) + (((((min((((v0 + v1) + 93)/32), (((v1 + 194)/32) + ((v2/8)*8))) + 1)/2) - (((min(v0, 101) + v1) + -227)/64))/14)*14)))"),
(3, "((min((((v0 + v1) + -1667)/128), (((v1 + -254)/128) + ((v2/16)*16))) + 15) <= ((((min(v0, 1413) + v1) + -1539)/128) + ((((min((((v0 + v1) + 381)/128), (((v1 + 1794)/128) + ((v2/16)*16))) - (((min(v0, 1413) + v1) + -1667)/128)) + -1)/2)*2)))"),
(3, "((min((((v0 + v1) + -1667)/128), (((v1 + -254)/128) + ((v2/16)*16))) + 15) <= ((((min(v0, 1413) + v1) + -771)/128) + ((((min((((v0 + v1) + 381)/128), (((v1 + 1794)/128) + ((v2/16)*16))) - (((min(v0, 1413) + v1) + -1667)/128)) + -1)/8)*8)))"),
(3, "(((min(((v0 - v1)/16), v2)*16) + v1) <= (max(((v2*16) + (v1 - v0)), -15) + min((((v2*16) + v1) + 15), v0)))"),
(3, "(((min(((((((v0 - v1) + 1)/8)*8) + v1) + 6), v0)/2) + 1) <= (((v2 + 89)/2) + (((((min(((((((v0 - v1) + 9)/8)*8) + v1) + -2), v0)/2) - ((v2 + -9)/2)) + 1)/50)*50)))"),
(3, "((min(((((((v0 - v1) + 1)/8)*8) + v1) + 6), v0) + -41) <= (((((min(((((((v0 - v1) + 9)/8)*8) + v1) + -2), v0) - v2) + 7)/49)*49) + v2))"),
(3, "((min(((((((v0 - v1) + 1)/8)*8) + v1) + 6), v0) + -89) <= (((((min(((((((v0 - v1) + 9)/8)*8) + v1) + -2), v0) - v2) + 7)/97)*97) + v2))"),
(3, "(((min((((((v0 - v1) + 191)/16)*16) + v1), (v0 + 176)) + -77)/2) <= ((v2/2) + ((((((min((((((v0 - v1) + 207)/16)*16) + v1), (v0 + 192)) + 1)/2) - (v2/2)) + 1)/49)*49)))"),
(3, "((min(((((((v0 - v1) + 2)/16)*16) + v1) + 13), v0) + 3) <= min((min((((((min((((((v0 - v1) + 18)/16)*16) + v1), (v0 + 3)) - v2) + 12)/16)*16) + v2), v0) + 3), (((((v0 - v1) + 18)/16)*16) + v1)))"),
(3, "((min((((v0 + v1) + -23)/4), (((v1 + -6)/4) + ((v2/8)*8))) + 7) <= ((((min(v0, 17) + v1) + 749)/4) + ((((min((((v0 + v1) + 9)/4), (((v1 + 26)/4) + ((v2/8)*8))) - (((min(v0, 17) + v1) + -23)/4)) + -1)/194)*194)))"),
(3, "(((min((((v0 + v1) + -23)/4), (((v1 + -6)/4) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 17) + v1) + 353)/8) + (((((min((((v0 + v1) + 9)/4), (((v1 + 26)/4) + ((v2/8)*8))) + 1)/2) - (((min(v0, 17) + v1) + -31)/8))/49)*49)))"),
(3, "(((min((((v0 + v1) + -23)/4), (((v1 + -6)/4) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 17) + v1) + 745)/8) + (((((min((((v0 + v1) + 9)/4), (((v1 + 26)/4) + ((v2/8)*8))) + 1)/2) - (((min(v0, 17) + v1) + -31)/8))/98)*98)))"),
(3, "(((min((((v0 + v1) + -23)/4), (((v1 + -6)/4) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 17) + v1) + -7)/8) + (((((min((((v0 + v1) + 9)/4), (((v1 + 26)/4) + ((v2/8)*8))) + 1)/2) - (((min(v0, 17) + v1) + -31)/8))/4)*4)))"),
(3, "(((min((v0 - ((v1*26) + v2)), 25) + (v1*26)) + v2) <= min((((v1*26) + v2) + 25), v0))"),
(3, "(((min(((v0 - v1)/26), v2)*26) + v1) <= (max(((v2*26) + (v1 - v0)), -25) + min((((v2*26) + v1) + 25), v0)))"),
(3, "((min(((((((v0 - v1) + 2)/8)*8) + v1) + 5), v0) + 3) <= min((min((((((min((((((v0 - v1) + 10)/8)*8) + v1), (v0 + 3)) - v2) + 4)/8)*8) + v2), v0) + 3), (((((v0 - v1) + 10)/8)*8) + v1)))"),
(6, "(((min(((((((v0 - v1) + 2)/8)*8) + v1) + 5), v0) + 3) <= min((min((((((min((((((v0 - v1) + 10)/8)*8) + v1), (v0 + 3)) - v2) + 4)/8)*8) + v2), v0) + 3), (((((v0 - v1) + 10)/8)*8) + v1))) and (((min(((v3 - v4)/13), v5)*13) + v4) <= (max(((v5*13) + (v4 - v3)), -12) + min((((v5*13) + v4) + 12), v3))))"),
(3, "((min(((((((v0 - v1) + 2)/8)*8) + v1) + 5), v0) + -9) <= (((((min((((((v0 - v1) + 10)/8)*8) + v1), (v0 + 3)) - v2) + 4)/17)*17) + v2))"),
(3, "((min(((((((v0 - v1) + 4)/16)*16) + v1) + 11), v0) + 5) <= min((min((((((min((((((v0 - v1) + 20)/16)*16) + v1), (v0 + 5)) - v2) + 10)/16)*16) + v2), v0) + 5), (((((v0 - v1) + 20)/16)*16) + v1)))"),
(6, "(((min(((((((v0 - v1) + 4)/16)*16) + v1) + 11), v0) + 5) <= min((min((((((min((((((v0 - v1) + 20)/16)*16) + v1), (v0 + 5)) - v2) + 10)/16)*16) + v2), v0) + 5), (((((v0 - v1) + 20)/16)*16) + v1))) and (((min(((v3 - v4)/26), v5)*26) + v4) <= (max(((v5*26) + (v4 - v3)), -25) + min((((v5*26) + v4) + 25), v3))))"),
(6, "(((min(((((((v0 - v1) + 4)/16)*16) + v1) + 11), v0) + 5) <= min((min((((((min((((((v0 - v1) + 20)/16)*16) + v1), (v0 + 5)) - v2) + 10)/16)*16) + v2), v0) + 5), (((((v0 - v1) + 20)/16)*16) + v1))) and (((min((((v3 - v4) + 4)/26), v5)*26) + v4) <= (max(((v5*26) + (v4 - v3)), -21) + min((((v5*26) + v4) + 21), v3))))"),
(3, "((min((((v0 + v1) + -43)/8), (((v1 + -14)/8) + ((v2/8)*8))) + 7) <= ((((min(v0, 29) + v1) + 733)/8) + ((((min((((v0 + v1) + 21)/8), (((v1 + 50)/8) + ((v2/8)*8))) - (((min(v0, 29) + v1) + -43)/8)) + -1)/98)*98)))"),
(3, "(((min((((v0 + v1) + -43)/8), (((v1 + -14)/8) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 29) + v1) + 325)/16) + (((((min((((v0 + v1) + 21)/8), (((v1 + 50)/8) + ((v2/8)*8))) + 1)/2) - (((min(v0, 29) + v1) + -59)/16))/25)*25)))"),
(3, "(((min((((v0 + v1) + -43)/8), (((v1 + -14)/8) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 29) + v1) + 725)/16) + (((((min((((v0 + v1) + 21)/8), (((v1 + 50)/8) + ((v2/8)*8))) + 1)/2) - (((min(v0, 29) + v1) + -59)/16))/50)*50)))"),
(3, "((min(((((((v0 - v1) + 4)/8)*8) + v1) + 3), v0) + 5) <= min((min((((((min((((((v0 - v1) + 12)/8)*8) + v1), (v0 + 5)) - v2) + 2)/8)*8) + v2), v0) + 5), (((((v0 - v1) + 12)/8)*8) + v1)))"),
(3, "(((min(((v0 - v1)/52), v2)*52) + v1) <= (max(((v2*52) + (v1 - v0)), -51) + min((((v2*52) + v1) + 51), v0)))"),
(3, "((min(((((((v0 - v1) + 8)/16)*16) + v1) + 7), v0) + 9) <= min((min((((((min((((((v0 - v1) + 24)/16)*16) + v1), (v0 + 9)) - v2) + 6)/16)*16) + v2), v0) + 9), (((((v0 - v1) + 24)/16)*16) + v1)))"),
(6, "(((min(((((((v0 - v1) + 8)/16)*16) + v1) + 7), v0) + 9) <= min((min((((((min((((((v0 - v1) + 24)/16)*16) + v1), (v0 + 9)) - v2) + 6)/16)*16) + v2), v0) + 9), (((((v0 - v1) + 24)/16)*16) + v1))) and (((min(((v3 - v4)/26), v5)*26) + v4) <= (max(((v5*26) + (v4 - v3)), -25) + min((((v5*26) + v4) + 25), v3))))"),
(9, "(min((((v0 + v1)*81) + (min(((v2*41) + (((v3*2) + v4) + v5)), v6) + v7)), v8) <= (((v0 + v1)*81) + (((v2*41) + (((v3*2) + v4) + v5)) + v7)))"),
(3, "((min((((v0 + v1) + -83)/16), (((v1 + -30)/16) + ((v2/8)*8))) + 7) <= ((((min(v0, 53) + v1) + 301)/16) + ((((min((((v0 + v1) + 45)/16), (((v1 + 98)/16) + ((v2/8)*8))) - (((min(v0, 53) + v1) + -83)/16)) + -1)/25)*25)))"),
(3, "(((min((((v0 + v1) + -83)/16), (((v1 + -30)/16) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 53) + v1) + -19)/32) + (((((min((((v0 + v1) + 45)/16), (((v1 + 98)/16) + ((v2/8)*8))) + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/4)*4)))"),
(3, "(((min((((v0 + v1) + -83)/16), (((v1 + -30)/16) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 53) + v1) + 269)/32) + (((((min((((v0 + v1) + 45)/16), (((v1 + 98)/16) + ((v2/8)*8))) + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/13)*13)))"),
(3, "(((min((((v0 + v1) + -83)/16), (((v1 + -30)/16) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 53) + v1) + 685)/32) + (((((min((((v0 + v1) + 45)/16), (((v1 + 98)/16) + ((v2/8)*8))) + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/26)*26)))"),
(3, "(((min((((v0 + v1) + -83)/16), (((v1 + -30)/16) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 53) + v1) + -83)/32) + (((((min((((v0 + v1) + 45)/16), (((v1 + 98)/16) + ((v2/8)*8))) + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/2)*2)))"),
(3, "((min((((v0 + v1) + -835)/64), (((v1 + -126)/64) + ((v2/16)*16))) + 15) <= ((((min(v0, 709) + v1) + -3)/64) + ((((min((((v0 + v1) + 189)/64), (((v1 + 898)/64) + ((v2/16)*16))) - (((min(v0, 709) + v1) + -835)/64)) + -1)/14)*14)))"),
(3, "((min((((v0 + v1) + -835)/64), (((v1 + -126)/64) + ((v2/16)*16))) + 15) <= ((((min(v0, 709) + v1) + -387)/64) + ((((min((((v0 + v1) + 189)/64), (((v1 + 898)/64) + ((v2/16)*16))) - (((min(v0, 709) + v1) + -835)/64)) + -1)/7)*7)))"),
(3, "((min((((v0 + v1) + -835)/64), (((v1 + -126)/64) + ((v2/16)*16))) + 15) <= ((((min(v0, 709) + v1) + -643)/64) + ((((min((((v0 + v1) + 189)/64), (((v1 + 898)/64) + ((v2/16)*16))) - (((min(v0, 709) + v1) + -835)/64)) + -1)/4)*4)))"),
(3, "((min((((((v0 - v1)/8)*8) + v1) + 7), v0) + -16) <= ((((min((((((v0 - v1)/8)*8) + v1) + 7), v0) - v2)/17)*17) + v2))"),
(3, "((min((((((v0 - v1)/8)*8) + v1) + 7), v0) + -34) <= ((((min((((((v0 - v1)/8)*8) + v1) + 7), v0) - v2)/35)*35) + v2))"),
(3, "(((min((v0 - ((v1*8) + v2)), 7) + (v1*8)) + v2) <= min((((v1*8) + v2) + 7), v0))"),
(2, "(((min(((((v0 - v1) + 98)/97)*97), 8) + v1) + -8) <= v1)"),
(3 ,"((v0 < v1) and (((v1 + v2) + 21)/8) <= (((v1 + v2) + 22)/8)) or ((v0 >= v1) and ((((v1 + v2) + -14)/8) <= (((v1 + v2) + 22)/8)))"),
]

# Do not scale
# (7, "(max(max(min(v0, 12), (min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(((v1 + -15)/16), (v2 + -1)), ((v1 + -14)/16)), ((v1 + -13)/16)), ((v1 + -2)/16)), ((v1 + -1)/16)), ((v1 + 1)/16)), ((v3 + -2)/16)), ((v3 + -1)/16)), ((v4 + -2)/16)), ((v4 + -1)/16)), ((v5 + -2)/16)), ((v5 + -1)/16)), ((v6 + -2)/16)), ((v6 + -1)/16)), 11) + 1)), 0) <= max(min(v0, 12), 0))"),
# (10, "(max(max(min(((v0 + 131)/144), 2), (min(((min((min(min(min(min(min(min((min((((v1 + v2) + 25)/2), v3) - ((v4*288) + v5)), v6), (min((((v1 + v2) + 29)/2), v3) - ((v4*288) + v5))), (v7 + 13)), v8), v9), (v7 + 15)) + 128), v8) + -140)/144), 1) + 1)), 0) <= max(min(((v0 + 131)/144), 2), 0))"),
# (7, "(max(max(min(v0, 24), (min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(((v1 + -15)/16), (v2 + -1)), ((v1 + -14)/16)), ((v1 + -13)/16)), ((v1 + -2)/16)), ((v1 + -1)/16)), ((v1 + 1)/16)), ((v3 + -2)/16)), ((v3 + -1)/16)), ((v4 + -2)/16)), ((v4 + -1)/16)), ((v5 + -2)/16)), ((v5 + -1)/16)), ((v6 + -2)/16)), ((v6 + -1)/16)), 23) + 1)), 0) <= max(min(v0, 24), 0))"),
# (18, "(min(min(min(min(((v0 - ((v1*144) + v2)) + 2), v3), (v3 + 1)), (min(min(min(min(min(min(min(min(min(min(v4, v5), v6), v7), v8), v9), v10), v11), v12), ((((v13 + v14) + -55)/4) - ((v1*144) + v2))), ((((v13 + v14) + -54)/4) - ((v1*144) + v2))) + 16)), (v15 + 17)) <= 12)"),
# (5, "(((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + -1)/8)*8)), (v3 + -8)) + -15)/2) <= ((v4/2) + ((((((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + 7)/8)*8)), v3) + 1)/2) - (v4/2)) + 1)/14)*14)))"),
# (, "(max(max(min(v0, 2), (min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min((min(min(min(v1, v2), v3), v4) + -1), v2), ((v5 + -208)/192)), ((v5 + -207)/192)), ((v5 + -206)/192)), ((v5 + -205)/192)), ((v5 + -191)/192)), ((v5 + -4)/192)), ((v5 + -3)/192)), ((v5 + -2)/192)), ((v5 + -1)/192)), ((v6 + -210)/192)), ((v6 + -209)/192)), ((v6 + -208)/192)), ((v6 + -207)/192)), ((v6 + -206)/192)), ((v6 + -205)/192)), ((v6 + -204)/192)), ((v6 + -203)/192)), ((v6 + -194)/192)), ((v6 + -193)/192)), ((v6 + -191)/192)), ((v6 + -190)/192)), ((v6 + -189)/192)), ((v6 + -4)/192)), ((v6 + -3)/192)), ((v6 + -2)/192)), ((v6 + -1)/192)), ((v6 + 1)/192)), ((v6 + 2)/192)), ((v6 + 3)/192)), (((((((v7 + v8) + -209)/2)*2) - ((v9*384) + v10)) + -1)/192)), ((v11 + -1)/192)), ((v12 + -1)/192)), (((((((v7 + v8) + -203)/2)*2) - ((v9*384) + v10)) + -1)/192)), ((v13 + -1)/192)), ((v14 + -1)/192)), ((v15 + -1)/192)), (((((((v7 + v8) + -31)/2)*2) - ((v9*384) + v10)) + -178)/192)), ((v16 + -178)/192)), ((v17 + -184)/192)), ((v17 + -182)/192)), ((v17 + -178)/192)), ((v18 + -184)/192)), ((v18 + -182)/192)), ((v19 + -178)/192)), ((v20 + -182)/192)), ((v20 + -178)/192)), ((v21 + -182)/192)), ((v22 + -2)/192)), ((v22 + -1)/192)), ((v23 + -2)/192)), ((v23 + -1)/192)), ((v24 + -4)/192)), ((v24 + -2)/192)), ((v24 + -1)/192)), ((v25 + -4)/192)), ((v25 + -2)/192)), ((v25 + -1)/192)), 1) + 1)), 0) <= max(min(v0, 2), 0))"),
# (, "(max(max(min(v0, 2), (min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min((min(min(min(v1, v2), v3), v4) + -1), v2), ((v5 + -191)/192)), ((v5 + -2)/192)), ((v5 + -1)/192)), ((v6 + -210)/192)), ((v6 + -209)/192)), ((v6 + -208)/192)), ((v6 + -207)/192)), ((v6 + -206)/192)), ((v6 + -205)/192)), ((v6 + -204)/192)), ((v6 + -203)/192)), ((v6 + -194)/192)), ((v6 + -193)/192)), ((v6 + -191)/192)), ((v6 + -190)/192)), ((v6 + -189)/192)), ((v6 + -4)/192)), ((v6 + -3)/192)), ((v6 + -2)/192)), ((v6 + -1)/192)), ((v6 + 1)/192)), ((v6 + 2)/192)), ((v6 + 3)/192)), (((((((v7 + v8) + -209)/2)*2) - ((v9*384) + v10)) + -1)/192)), ((v11 + -1)/192)), ((v12 + -1)/192)), (((((((v7 + v8) + -203)/2)*2) - ((v9*384) + v10)) + -1)/192)), ((v13 + -1)/192)), ((v14 + -1)/192)), ((v15 + -1)/192)), (((((((v7 + v8) + -31)/2)*2) - ((v9*384) + v10)) + -178)/192)), ((v16 + -178)/192)), ((v17 + -184)/192)), ((v17 + -182)/192)), ((v17 + -178)/192)), ((v18 + -184)/192)), ((v18 + -182)/192)), ((v19 + -178)/192)), ((v20 + -182)/192)), ((v20 + -178)/192)), ((v21 + -182)/192)), ((v22 + -2)/192)), ((v22 + -1)/192)), ((v23 + -2)/192)), ((v23 + -1)/192)), ((v24 + -4)/192)), ((v24 + -2)/192)), ((v24 + -1)/192)), ((v25 + -4)/192)), ((v25 + -2)/192)), ((v25 + -1)/192)), 1) + 1)), 0) <= max(min(v0, 2), 0))"),
# (, "(max(max(min(v0, 2), (min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min((min(v1, v2) + -1), v2), ((v3 + -191)/192)), ((v3 + -2)/192)), ((v3 + -1)/192)), ((v4 + -194)/192)), ((v4 + -193)/192)), ((v4 + -191)/192)), ((v4 + -190)/192)), ((v4 + -189)/192)), ((v4 + -2)/192)), ((v4 + -1)/192)), ((v4 + 1)/192)), ((v4 + 2)/192)), ((v4 + 3)/192)), (((((((v5 + v6) + -193)/2)*2) - ((v7*384) + v8)) + -1)/192)), ((v9 + -1)/192)), (((((((v5 + v6) + -189)/2)*2) - ((v7*384) + v8)) + -1)/192)), (((((((v5 + v6) + -15)/2)*2) - ((v7*384) + v8)) + -178)/192)), ((v10 + -182)/192)), ((v10 + -178)/192)), (((((((v5 + v6) + -11)/2)*2) - ((v7*384) + v8)) + -182)/192)), ((v11 + -2)/192)), ((v11 + -1)/192)), ((v12 + -2)/192)), ((v12 + -1)/192)), ((v13 + -2)/192)), ((v13 + -1)/192)), 1) + 1)), 0) <= max(min(v0, 2), 0))"),
 





import islpy as isl
import time
import signal

DEBUG = True

class TimedOutExc(Exception):
  pass

def deadline(timeout, *args):
  def decorate(f):
    def handler(signum, frame):
      raise TimedOutExc()

    def new_f(*args):

      signal.signal(signal.SIGALRM, handler)
      signal.alarm(timeout)
      return f(*args)
      signa.alarm(0)

    new_f.__name__ = f.__name__
    return new_f
  return decorate


# Read the set s from a string and prove that it is not empty
@deadline(1)
def read_and_prove(s):
    isl_s = isl.Set(s)
    if DEBUG:
	print "ISL set: ", isl_s
    empty_s = isl_s.is_empty()
    return empty_s


# Take an expression e (expressed as a string) and add any necessary
# constraints and transform it into a set (add dimensions, ...). The output
# is still a string representation.  dim is the number of dimensions.
def construct_s(dim, e):
    res = "{ S["
    for i in range(0, dim):
	if i != 0:
	    res = res + ", "
	res = res + "v" + str(i)
    res = res + "] : "
    for i in range(0, dim):
	if i != 0:
	    res = res + " and "
	res = res + "v" + str(i) + " > 0"
    res = res + " and " + e + "}"
    return res

# (5, "(((((v0 + v1)/2) + ((v2 + v3)*4)) + -2) <= select((v4 < v1), ((((v0 + v1) + 3)/2) + ((v2 + v3)*4)), ((((v0 + v1)/2) + ((v2 + v3)*4)) + -1)))"),

def main():
    i = 0
    total_time = 0
    for e in expressions:
	print "Set: ", str(i)
	s = construct_s(e[0], e[1])
	print "Constructed set: ", s
	start_time = time.time()
	empty_s = read_and_prove(s)
	end_time = time.time()
	print "Empty? ", empty_s
	current_time = (end_time - start_time)
	total_time = total_time + current_time
	print "Time:", current_time
	print "---------------------------------"
	i = i + 1
    print "Number of expressions: ", len(expressions)
    print "Total time: ", total_time, " s"

main()
